d-partial-world(D;f;t';s;d)
== <i,x. M(i).ds(x)
== , i,a. M(i).da(locl(a))
== , l,tg. M(source(l)).dout(l,tg)
== , i,t. if t <z t' then (f(t,i)).1 else s(i) fi 
== , i,t. if t <z t' then ((f(t,i)).2).1 else null fi 
== , i,t. if t <z t' then (f(t,i)).2.2 else [] fi 
== , i.NullMachine
== , d
== , > 

latex

---

clarification:

d-partial-world(D;f;t';s;d)
== <i,x. d-m(D; i).ds(x)
== , i,a. d-m(D; i).da(locl(a))
== , l,tg. d-m(D; source(l)).dout(l,tg)
== , i,t. if t <z t' then (f(t,i)).1 else s(i) fi 
== , i,t. if t <z t' then ((f(t,i)).2).1 else null fi 
== , i,t. if t <z t' then (f(t,i)).2.2 else [] fi 
== , i.NullMachine
== , d
== , > 

latex

Definitions	M.ds(x), M.da(a), locl(a), M.dout(l,tg), M(i), source(l), t.1, null, if b then t else f fi , i <z j, t.2, f(a), [], x.A(x), NullMachine, <a, b>,
FDL editor aliases	d-partial-world